(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-verbose "Scope checking Agda.Primitive ")
(agda2-verbose "Building interface... ")
(agda2-verbose "Writing interface file _build/2.6.3/agda/Debug.agdai. ")
(agda2-verbose "Wrote interface file. ")
(agda2-verbose "Accumulated statistics. ")
(agda2-verbose "Finished Debug. ")
(agda2-verbose " current options = [--safe: False, --without-K: False, --no-universe-polymorphism: False, --no-cumulativity: True, --cubical/--erased-cubical: False, --guarded: False, --prop: False, --two-level: False, --rewriting: False, --sized-types: False, --guardedness: False] ")
(agda2-verbose " imported options = [--safe: False, --without-K: False, --no-universe-polymorphism: False, --no-cumulativity: True, --cubical/--erased-cubical: False, --guarded: False, --prop: False, --two-level: False, --rewriting: False, --sized-types: False, --guardedness: False] ")
(agda2-verbose " Now we've looked at Debug ")
(agda2-status-action "Checked")
(agda2-info-action "*All Done*" "" nil)
((last . 1) . (agda2-goals-action '()))
